A:Type, eq:EqDecider(A), L:A List, v:Top, x:A. x  dom(L fpf v)  (x  L) 

latex

Definitions	t  T, x:A. B(x), EqDecider(T), Top, (x  l), P  Q, P  Q, P & Q, P  Q, deq-member(eq;x;L), b, Prop, x. t(x), x  dom(f), L fpf v
Lemmas	all functionality wrt iff, iff functionality wrt iff, assert-deq-member, iff wf, assert wf, deq-member wf, l member wf, top wf, deq wf